Nuprl Lemma : l_before_select
11,40
postcript
pdf
T
:Type,
L
:(
T
List),
i
,
j
:int_seg(0; ||
L
||). (
j
<
i
)
l_before(
L
[
j
];
L
[
i
];
L
;
T
)
latex
Definitions
prop{i:l}
,
t
T
,
l_before(
x
;
y
;
l
;
T
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
int_seg(
i
;
j
)
Lemmas
length
wf1
,
int
seg
wf
,
sublist
pair
origin
T:Type, L:(T List), i,j:int_seg(0; ||L||). (j < i) 
l_before(L[j]; L[i]; L; T) T:Type, L:(T List), i,j:int_seg(0; ||L||). (j < i) l_before(L[j]; L[i]; L; T) 
T Qx:A. B(x)